@InProceedings{RomeroAmbrSouz:2012:FiStVe,
               author = "Romero, Alessandro Gerlinger and Ambrosio, Ana Maria and Souza, 
                         Marcelo Lopes de Oliveira e",
          affiliation = "{} and {Instituto Nacional de Pesquisas Espaciais (INPE)} and 
                         {Instituto Nacional de Pesquisas Espaciais (INPE)}",
                title = "Finite state-machine verification applied to hybrid systems",
            booktitle = "Proceedings...",
                 year = "2012",
         organization = "Congresso SAE Brasil, 21.",
            publisher = "SAE",
             keywords = "state-machine, hybrid systems, source lines of code.",
             abstract = "The notion of a hybrid system is centered around a composition of 
                         discrete and continuous dynamics. In particular, the system has a 
                         continuous evolution and occasional jumps. The jumps correspond to 
                         the change of state in an automaton whose transitions are caused 
                         either by controllable or uncontrollable external events or by the 
                         continuous evolution. The continuous evolution and these jumps in 
                         control loops are the origins from the most stringent temporal 
                         demands. These temporal demands are one of the reasons that hybrid 
                         systems usually require a high level of safety. Inevitably this 
                         type of system is present in mobility devices such as cars, ships 
                         and aircraft. Works present data showing that SLOC (Source Lines 
                         Of Code), one controversial metric of complexity, growth at 
                         current rate using existing development practices will seriously 
                         impact affordability of the next generation of commercial aircraft 
                         (remarkable hybrid systems). Efforts to develop this type of 
                         system have increasingly suffered from cost and schedule overruns. 
                         These trends are largely attributed to: (a) increasing system 
                         complexity, driven by requirements for increased functionality, 
                         performance and dependability; (b) using inadequate development 
                         practices. In fact, the verification of such systems has become a 
                         key activity in the development life-cycle. Historically such 
                         activity demands experts and high efforts, and uses ad-hoc 
                         methods. Therefore, the aim of this work is to apply the vast 
                         theory of automatic test case generation for this type of system, 
                         showing an effective and reproducible alternative for automatic 
                         test case generation based on finite state-machines. A case study 
                         that was developed considering the problem of inverted pendulum 
                         evaluates the suggested approach. The inverted pendulum is a model 
                         of attitude control for satellite launch vehicles at its departure 
                         (the objective of the attitude control problem is to keep the 
                         vehicle in a vertical position). The uniqueness of an inverted 
                         pendulum, due to its natural instability, provides various 
                         researches in areas of control, electronics and software. 
                         Furthermore, the inverted pendulum is a classic hybrid system, 
                         since it is composed of continuous dynamic (stabilization of the 
                         pendulum in a vertical axis) and discrete (failure mode 
                         management). This case study has given strong indications that the 
                         approach can bring significant gains for the effectiveness coupled 
                         with the reduction of time for planning and execution of 
                         verification, as well as contributing to fulfill certification 
                         requirements.",
  conference-location = "S{\~a}o Paulo",
      conference-year = "2012",
                 isbn = "2012-36-0429",
                label = "lattes: 3237709114127674 1 RomeroAmbrSouz:2012:FiStVe",
             language = "en",
           targetfile = "romero_finite.pdf",
        urlaccessdate = "30 abr. 2024"
}